\section{Matematyka klasyczna} \label{sec:matematyka-klasyczna}
Przez matematykę klasyczną rozumie się matematykę nauczaną w szkołach, używaną w inżynierii i nauce.
Przyjmuje się, że formalnymi podstawami matematyki klasycznej jest teoria mnogości. Podstawą teorii mnogości jest rachunek logiczny pierwszego rzędu i aksjomaty Zermelo-Fraenkla z aksjomatem wyboru (zwyczajowo nazywane \emph{ZFC}: Zermelo–Fraenkel + Choice) \cite{ciesielski}.
\subsection{Nieformalność} \label{subsec:nieformalnost}
Matematyka klasyczna zazwyczaj jest stosowana nieformalnie, to znaczy bez odniesienia do postaw formalnych. Proszę zwrócić uwagę, że bez odniesienia do podstaw (jak na przykład: definicji liczb naturalnych) nie da się podać dowodu twierdzenia o przemienności dodawania liczb naturalnych innego niż ``to widać''.
\begin{theorem}
  \[ \forall a,b \in \mathbb{N}: a + b = b + a \]
\end{theorem} 
\begin{proof}
  Zależy od przyjętej definicji liczb naturalnych i dodawania.   %może dowód w Agdzie w załączniku?
\end{proof}
Możliwymi definicjami liczb naturalnych są między innymi \cite{natural-numbers-def}: postulaty Peano, Konstrukcja Fregego-Russella \cite{russel}, model Von Neumana. W Agdzie liczby naturalne definiuje się zazwyczaj przez postulaty Peano (przykład: (\ref{subsection:definicja-typow-indukcyjnych})).

Zwyczajowe, nieformalne podejście do matematyki powoduje że pierwszym krokiem do komputerowego sprawdzenia twierdzenia jest uzupełnienie braków w formalizmie dowodu.
\subsection{Niekonstruktywność} \label{sec:niekonstruktywnost}
Matematka klasyczna pozwala dowodzić istnienia pewnych obiektów matematycznych bez podania ich konstrukcji. Na przykład, korzystając z silnego prawa podwójnego przeczenia (\( \forall p : \neg \neg p \implies p \)) można dowieść prawdziwości \( p \) przez pokazanie, że \( p \) nie może nie istnieć.\footnote{W teorii typów {\PerMartinLofDopelniacz} \(\neg p\) interpretuje się jako \(p \rightarrow \bot\),  co oznacza, że \(\neg \neg p \) odpowiada \( (p \rightarrow \bot) \rightarrow \bot\).} 

Z kolei prawo wyłączonego środka (\(\forall p : p \lor \neg p \)) oznacza, że każdej hipotezie odpowiada dowód tej hipotezy lub dowód jej zaprzeczenia, nie wymagając podania konstrukcji jedego z dowodów.\footnote{W teorii typów {\PerMartinLofDopelniacz} \(A + \neg A \) (dla zadanego \(A : \mathcal{U}_i\)) nazywa się \emph{rozstrzygalnością} typu \(A\) i wymaga podania konstrukcji dowodu hipotezy lub jej zaprzeczenia. W niektórych odmianach teorii, np w Homotopicznej Teroii Typów można udowodnić że nie wszystkie typy są rozstrzygalne \cite{hottbook}.}

Programy komputerowe są z natury konstruktywne, niekonstruktywność utrudnia interpretację twierdzenia matematycznego jako programu komputerowego przyjmującego hipotezę i zwracającego dowód (izomorfizm Curry’ego-Howarda \cite{howard}).
